@kfriedberger: Could you have a look at the last commit that adds multi-arch support? I've tried it for arm64 with qemu, but I don't have a windows machine to test the binaries. (You'll have to use the repository from the CVC5 pull request here if you want to build the binaries yourself)

The missing pull request for CVC5 has now been merged and we can build from main

The proof generation/traversal API has changed compared to older versions. Do we include the new API and maybe even a native test for it?

If not, can we add that in this PR? It would be helpful for @gcarpio21 s proof interface.
(I can also do it, but probably in the later half of next week)

We compile the "full" API of CVC5, including all new features. I assume that the API changes from your comment refer to plain Java API. This should be done outside of this PR, as it might be independent of native code and low-level bindings. A separate PR would also allow to integrate this PR here soonish, and work on proofs later.

The proof generation/traversal API has changed compared to older versions. Do we include the new API and maybe even a native test for it?

If not, can we add that in this PR? It would be helpful for @gcarpio21 s proof interface. (I can also do it, but probably in the later half of next week)

For the purposes of correctly retrieving proofs from CVC5 I have written a test in the CVC5NativeAPITest class using some of the methods exposed in this version of CVC5 to handle proofs. I could add the test to this PR.

If there is just one additional test, then feel free to add it within this PR.

Update for the Windows build artifact:
There are remaining non-static dependencies to GCC-specific libraries. CVC5 packages them as additional libraries into the released archive:
https://github.com/cvc5/cvc5/blob/7bf5d3e457aa5c40b325b0e687de5a972b0dad4e/.github/actions/add-package/action.yml#L40-L42
We can do the same, and add those dependencies into Ivy and Maven. We would need to load those libraries before loading CVC5.

Improvement (future work, maybe within this PR):
CVC5 could be compiled "static", such that GCC-related dependencies are included. This would simplify development in JavaSMT and avoid potential conflicts with other SMT solvers.

Alternative (maybe future work, not part of this PR):
CVC5 has already a fully running build-system that publishes (nearly) static binaries for more platforms (see https://github.com/cvc5/cvc5/releases ). For other solvers, like Z3, we use the direct release instead of building our own binaries. This would only require to download several archives, and then repackage them according to our needs. This might allow us to even support MacOS on x64 and arm64 platform without any compilation overhead.

I added the test

Update for the Windows build artifact: There are remaining non-static dependencies to GCC-specific libraries. CVC5 packages them as additional libraries into the released archive: https://github.com/cvc5/cvc5/blob/7bf5d3e457aa5c40b325b0e687de5a972b0dad4e/.github/actions/add-package/action.yml#L40-L42

Ok, that's interesting. CVC5 actually seems to copy the .dll (or .so/dylib, depending on the platform) files into the jars they publish on their website. They're then extracted from the .jar at runtime and copied to a temporary folder by cvc5.Utils.loadLibraries() where they're then loaded from. We disabled this loader mechanism and use NativeLibraries instead, but if we switch to the .jars from the CVC5 website we might not need to include any binaries at all. Then again we would have to load a different version of cvc5.jar for each platform (so that it includes the right binaries).

We can do the same, and add those dependencies into Ivy and Maven. We would need to load those libraries before loading CVC5.

Those libraries are the Mingw runtime and other solvers that are compiled with Mingw might also need them. Maybe there is a way to include them directly in JavaSMT to avoid conflicts between different versions for different solvers?

Alternatively we could also ask the CVC5 developers if they could add an option to statically link the Mingw runtime.

Alternatively we could also ask the CVC5 developers if they could add an option to statically link the Mingw runtime.

I've now asked the CVC5 for an option to include the MinGW runtime in static builds:
cvc5/cvc5#11756

@kfriedberger:
Could you try out the patch from the discussion (here) and check that it works on Windows?

I’m traveling for work these days and haven’t even read all my emails or had time for proper testing yet (that will happen the next days) 😄 , and there’s already a proposed solution that looks valid (https://gist.github.com/daniel-raffler/6f5c34b2a57380f90f026de0f1c09262) based on my comment and a related PR (cvc5/cvc5#11757) that even further simplifies the build and packaging scripts of CVC5! You all work at an incredible pace -- truly impressive! 🚀

I’m traveling for work these days and haven’t even read all my emails or had time for proper testing yet (that will happen the next days) 😄 , and there’s already a proposed solution that looks valid (https://gist.github.com/daniel-raffler/6f5c34b2a57380f90f026de0f1c09262) based on my comment and a related PR (cvc5/cvc5#11757) that even further simplifies the build and packaging scripts of CVC5! You all work at an incredible pace -- truly impressive! 🚀

Thanks! The PR has now been merged and is already included in the latest CVC5 dailies. I've opened a new branch here that fetches the binaries from the official CVC5 release and repackages them. This saves us quite some on the build and allows us to support macOS on both x64 and arm64 hardware.

If you'd like I could still add the commits to this PR. Or we wait and merge the other branch later?

Lets first finish this PR and then take a look at directly including CVC5 from the official webpage (see https://github.com/sosy-lab/java-smt/tree/cvc5-use-official-binaries).
I compiled CVC5 for Linux and Windows and published the artifact into Ivy and Maven.
I will update the tests and fix simple remaining issues here, then we merge this PR.